Nuprl Lemma : R-compat-Rplus-sq
0,22
postcript
pdf
A
,
B
,
C
:Top.
B
C
||
A
~ (
B
||
A
&
C
||
A
)
latex
Definitions
es
realizer
ind
Rplus
compseq
tag
def
,
Rnone?(
x1
)
,
Rplus-right(
x1
)
,
Rplus-left(
x1
)
,
Rplus?(
x1
)
,
Top
,
t
T
,
x
:
A
.
B
(
x
)
Lemmas
top
wf
origin
A, B, C:Top. B 
C || A ~ (B || A & C || A) A, B, C:Top. B C || A ~ (B || A & C || A) 
Tx:A. B(x)